Nuprl Lemma : ccsucc?_wf
11,40
postcript
pdf
x
:chain_config(). ccsucc?(
x
)
latex
Definitions
s
=
t
,
t
T
,
,
tt
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Id
,
ff
,
,
x
.
A
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
chain_config_ind(
x
;
head
;
tail
;
id
.
pred
(
id
);
id
,
num
.
succ
(
id
;
num
))
,
chain_config()
,
ccsucc?(
x
)
,
a
:
A
fp
B
(
a
)
,
strong-subtype(
A
;
B
)
,
P
Q
Lemmas
member
wf
,
chain
config
wf
,
chain
config
ind
wf
,
bool
wf
,
bfalse
wf
,
Id
wf
,
btrue
wf
,
nat
wf
origin
x:chain_config(). ccsucc?(x) 
x:chain_config(). ccsucc?(x) T
B(x)x:A. B(x)
x.A(x)
x,y. t(x;y)x. t(x) B(a)
Q